
\begin{figure*}[t]
\begin{center}
\begin{tabular}{|c|}
\hline
$\typerule{
  K \cup \{ \hl \},\Gamma \vdash \he:\hT
}{
  \KGdash \code{e;return l} : \Gamma(\hl)
}$~\RULE{(T-return)}
\quad
$\typerule{
  \mtype{}(\bot,\code{build},\code{C<FO,VI>})=\ol{\code{T}}\rightarrow\code{U}
    \gap
  \KGdash \ol{\he}:\ol{\code{T'}}
    \gap
  \KGdash \ol{\code{T'}} \st \ol{\code{T}}
}{
  \KGdash \code{new C<FO,VI>(}\ol{\he}\code{)} : \code{C<FO,VI>}
}$~\RULE{(T-New)}\\\\

$\typerule{
}{
  \KGdash \hx : \Gamma(\hx)
}$~\RULE{(T-Var)}
\quad
$\typerule{
}{
  \KGdash \code{null} : \hT
}$~\RULE{(T-null)}
\quad
$\typerule{
  \KGdash \he:\code{C<MO,IP>}
    \gap
  \ftype{}(\he,\hf,\code{C<MO,IP>})=\hT
}{
  \KGdash \he.\hf : \hT
}$~\RULE{(T-Field-Access)}\\\\

$\typerule{
}{
  \KGdash \hl : \Gamma(\hl)
}$~\RULE{(T-Location)}
\quad
$\typerule{
  \KGdash \he.\hf : \hT
    \gap
  \KGdash \code{e'}:\code{T'}
    \gap
  \KGdash \code{T'} \st \hT
    \gap
  \KGdash \he:\code{C<MO,IP>}
    \\
  \KGdash \code{IP} \st \Raw
    \gap
  \isTransitive(\he,\Gamma,\code{C<MO,IP>})
    \gap
  \code{MO} \neq \code{?}
}{
  \KGdash \he.\hf = \code{e'} : \code{T'}
}$~\RULE{(T-Field-Assignment)}\\\\

$\typerule{
  \KGdash \he_0:\code{C<MO,IP>}
    \gap
  \mtype{}(\he_0,\hm,\code{C<MO,IP>})=\ol{\code{T}}\rightarrow\code{T"}
    \gap
  \KGdash \ol{\he}:\ol{\code{T'}}
    \gap
  \KGdash \ol{\code{T'}} \st \ol{\code{T}}
    \gap
  \mguard{}(\hm,\code{C})=\code{IG}
    \\
  \KGdash \code{IP} \st \code{IG}
    \gap
  \code{IG}=\Raw \Rightarrow \isTransitive(\he_0,\Gamma,\code{C<MO,IP>})
    \gap
  \mtype{}(\hm,\code{C})=\ol{\code{U}}\rightarrow\code{V}
    \gap
  \Ofn{\code{T}_i}=\code{?} \Rightarrow \Ofn{\code{U}_i}=\code{?}
}{
  \KGdash \he_0\code{.m(}\ol{\he}\code{)} : \code{T"}
}$~\RULE{(T-Invoke)}\\


\hline
\end{tabular}
\end{center}
\caption{FOIGJ Expression Typing Rules ($\KGdash \he:\hT$).} %(casting, field access, and method invocation are the same as in FJ)
\label{Figure:expressions}
\end{figure*}
